r:Rng, a, b:|r|. (a +r b) = (b +r a)  |r| 

latex

Up	rings 1
Definitions of Statement	Rng
Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, x f y, Rng
Lemmas	rng wf, rng car wf, rng one wf, rng minus wf, rng times over plus, rng plus wf, rng plus inv assoc, rng plus assoc, rng times one, rng times over minus, rng plus zero, rng times zero, rng zero wf, rng plus inv, rng times wf